Definitions	Feasible(D), , P & Q, x:A. B(x), M(i), t  T, M.dout(l,tg), , M.din(l,tg), f(x)?z, t.1, t.2, mk-ma, , Top, if b then t else f fi , x  dom(f), deq-member(eq;x;L), reduce(f;k;as), ff, Y, b, M sends on link l, map(f;as), finite-type(T), False, x:A. B(x), , A  B, A, P  Q, , Surj(A;B;f), {i..j}, i  j < k
Lemmas	Id wf, IdLnk wf, ma-empty-feasible, top wf, le wf, int seg wf, surject wf, ldst wf, false wf